Ja, herzlich willkommen.

Ich werde gerade nach einem Detail zu den Übungen gefragt.

Moment.

Und zwar nochmal dazu, wie Pure Literal Elimination funktioniert, die in einer Übung vorkommt.

Pure Literal Elimination heißt deswegen so, weil sie dann anwendbar ist, wenn ein Literal in der CNF, die man gerade hat, nur in Reinform vorkommt.

Das heißt, nur ohne Negation davor.

Das heißt, El selber kann natürlich eine Negation haben, beispielsweise könnte El sowas sein wie Nicht A.

Und El kommt also Pure oder in Reinform in Phi vor, wenn eben El nur mit dieser Polarität in den Klauseln in Phi vorkommt und nie mit der gegensätzlichen Polarität.

Was wir dann machen, wenn das so ist, ist, wir ersetzen Phi durch Phi angenommen L, im selben Sinne, wie wir das getan hatten in unserem Korrektheitsbeweis für den Resolutionsalgorithmus.

Und das hier heißt, wenn wir uns erinnern, dass wir von den Klauseln in Phi das Gegenteil von L, also nicht L, das ist also, naja, wenn L selbst negiert ist, heißt das natürlich nicht, dass wir die Negation wegnehmen.

Ansonsten heißt es, wir fügen die Negation hinzu, dass wir also von den Klauseln in Phi das Nicht-El wegnehmen und zwar von denjenigen Klauseln, die das L nicht schon enthalten.

Und diejenigen Klauseln, die das L schon enthalten, die schmeißen wir ganz raus.

Der Gedanke dahinter ist, wenn L nur als L und nie als Nicht-El in Phi vorkommt, dann ist unsere beste Chance, das Ding wahr zu machen, L einfach auch wahr zu setzen.

Und dann sind ja alle Klauseln, die L enthalten, schon erledigt. Die können wir also vergessen.

Und aus allen anderen nehmen wir Nicht-El weg, weil wir keine Chance mehr haben, sie mittels Nicht-El wahr zu machen, weil wir ja schon L wahr gemacht haben.

Ich hoffe, das beantwortet auch die Frage von eben, ist das die Dame, die die Frage gestellt hatte, würden Sie damit die Frage als beantwortet empfinden?

Ja, gut, danke.

So.

Ja, wir haben letztes Mal die reine Syntax.

Die reine Syntax der Logik erster Stufe, also voll fast all logic kennengelernt.

Und wir folgen jetzt, wie schon mal angekündigt, nicht der Reihenfolge, wie wir sie in der Aussagenlogik verfolgt hatten,

dass wir also nach der Syntax erstmal die Semantik definieren und dann die Beweistheorie uns ansehen, sondern wir machen das umgekehrt.

Und zwar deswegen, weil die Beweistheorie, naja, nicht notwendig leichter zu verstehen ist als die Semantik, aber zumindest mal besser und sauberer hinzuschreiben ist als die Semantik, die eine Menge notationalen Dreck nach sich zieht, nämlich letztere.

Ja, wie gesagt, dagegen stellt sich also das mit dem natürlichen Schließen in voll relativ glatt dar.

Wir erweitern einfach die Regeln, die wir schon kennen, für Aussagenlogik, die sind also so weiterhin auf Logik erster Stufe anwendbar.

Also ist die Einführungsregel für Konjunktion, ist in Logik erster Stufe dieselbe wie die in Aussagenlogik.

Genauso für Disjunktion, Implikation, Negation und so weiter.

Wir müssen nur neue Regeln hinzufügen für die sprachlichen Ausdrucksmittel, die wir jetzt gegenüber Aussagenlogik hinzugefügt haben.

Das sind im Wesentlichen zwei Dinge, das sind einmal die Gleichheit und einmal die Quantoren.

Gleichheit ist wirklich relativ schnell abgehandelt, deswegen machen wir das erst.

Nach unserem bisherigen Vorgehen brauchen wir immer eine oder mehrere Einführungsregeln und eine oder mehrere Eliminationsregeln.

Und wir kommen in der Tat jeweils mit einer Regel aus.

Fangen wir an mit der Einführungsregel für Gleichheit. Ich muss also irgendwas voraussetzen und dann Gleichheit von irgendwas folgern.

Und in der Tat ist die Regel sehr simpel. Die Regel fängt einfach Reflexivität ein.

Also jeder Term ist gleich sich selbst. Gut, wird vermutlich keiner widersprechen wollen.

Und dann kommt die Eliminationsregel.

Da will ich jetzt also ausnutzen, dass ich schon weiß, dass zwei Terme E und D gleich sind.

Da gibt es nun viele verschiedene Arten, das zu machen und eine besonders mächtige Art, das zu tun, ist die folgende.

Ich stelle mir vor, ich wüsste irgendwas über E.

Dass ich irgendwas über E weiß, drückt sich darin aus, dass ich also eine Formel bewiesen habe, die ursprünglich mal eine freie Variable X hatte und für diese freie Variable habe ich E eingesetzt.

Also mit anderen Worten, ich habe irgendeine Formel bewiesen, in der E vorkommt.

Wenn ich also etwas über E weiß und ich weiß außerdem, dass E gleich D ist, dann weiß ich das natürlich auch über D.

Das heißt, ich folge an dieser Stelle, Phi mit D eingesetzt für X.

Auch das ist vielleicht nicht überraschend. Also alles, was ich über E weiß, weiß ich natürlich auch über alle zu E gleichen Dinge.

Was vielleicht daran jetzt ein bisschen überraschend ist, ist, dass es da dann schon aufhört.

Das sind alle Regeln, die ich jetzt für Gleichheit einführe.

So, nun wird man einwenden wollen, Mensch.

Da hat man sich doch eigentlich immer mehr Eigenschaften vorgestellt für Gleichheit. Zum Beispiel hätte man doch gedacht, dass Gleichheit symmetrisch ist.

Zum Beispiel, wenn ich also weiß, dass E gleich D ist, dann müsste ja auch D gleich E sein.

War schon gerade jemand sehr begeistert.